Definitions	Knd, false, true, True, b, False, 1of(t), 2of(t), x. t(x), IdLnk, Prop, Id, SQType(T), x:A. B(x), P  Q, {T}, t  T
Lemmas	Id sq, Id wf, IdLnk sq, IdLnk wf, pi2 wf, pi1 wf, assert wf, btrue wf, bfalse wf